bugfix: symbol_factoryt must preserve struct_tag types [blocks: #3652] #3647
Conversation
The struct_tag type is currently expanded into the corresponding struct type; this yields an invalid assignment instruction where the type of lhs() and rhs() differs.
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: b552cc1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/95950695
There was a problem hiding this comment.
Quoting part of the commit message: "this yields an invalid assignment instruction where the type of lhs() and rhs() differs."
Why did we not notice that that's invalid, and could we have a regression test that failed before and is fixed via this change? My suspicion, however, is that what was generated will only become "invalid" via some future change (the symex type renaming story). So we either need
- a regression test or
- an accurate commit message.
A lot of effort is going into validation of goto programs and I'm finding it hard to approve of "bug fixes" of this sort that come without any tests or additional goto-program validation steps. For any bug that we fix we better make sure it cannot come up again. And if isn't a bug just yet, then we shouldn't say so.
|
The problem is that the Java object factory has the same issue; that needs to be fixed before the goto-program validation check can be enabled. |
tautschnig
changed the title
tautschnig
dismissed
their stale review
My concerns have been resolved via #3660
The struct_tag type is currently expanded into the corresponding struct
type; this yields an invalid assignment instruction where the type of lhs()
and rhs() differs.